[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification encoding-superblock
instantiate parameter
   elem, 
   encoding-elem-alignment

< 
   encoding-aligned

with 
   superblock, 
   eraseblock


   
by mapping
      : elem → superblock; 
      ENCODED_ELEM_ALIGNMENT → EB_PAGE_SIZE; 
      a → sb; 
      b → sb0; 
      c → sb1
   rename 
      encoding-size → encoding-size-unaligned; 
      size-aligned → encoding-size; 
      is-garbage → is-garbage-sb-unaligned; 
      is-encoded → is-encoded-unaligned; 
      is-encoded-aligned → is-encoded; 
      encode_aligned# → encode_superblock#; 
      encode# → encode_superblock_unaligned#; 
      decode_aligned# → decode_superblock#; 
      decode# → decode_superblock_unaligned#
end instantiate